The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y)) → cons(Y)
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The following defined symbols can occur below the 0th argument of add: sqr, add, dbl
The following defined symbols can occur below the 1th argument of add: dbl

Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
half(dbl(X)) → X

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

add(s(X), Y) → s(add(X, Y))
half(s(0)) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
half(s(s(X))) → s(half(X))
half(0) → 0
first(0, X) → nil
dbl(s(X)) → s(s(dbl(X)))
first(s(X), cons(Y)) → cons(Y)
sqr(0) → 0
add(0, X) → X
terms(N) → cons(recip(sqr(N)))

Rewrite Strategy: INNERMOST

(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

add(s(X), Y) → s(add(X, Y)) [1]
half(s(0)) → 0 [1]
sqr(s(X)) → s(add(sqr(X), dbl(X))) [1]
dbl(0) → 0 [1]
half(s(s(X))) → s(half(X)) [1]
half(0) → 0 [1]
first(0, X) → nil [1]
dbl(s(X)) → s(s(dbl(X))) [1]
first(s(X), cons(Y)) → cons(Y) [1]
sqr(0) → 0 [1]
add(0, X) → X [1]
terms(N) → cons(recip(sqr(N))) [1]

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

add(s(X), Y) → s(add(X, Y)) [1]
half(s(0)) → 0 [1]
sqr(s(X)) → s(add(sqr(X), dbl(X))) [1]
dbl(0) → 0 [1]
half(s(s(X))) → s(half(X)) [1]
half(0) → 0 [1]
first(0, X) → nil [1]
dbl(s(X)) → s(s(dbl(X))) [1]
first(s(X), cons(Y)) → cons(Y) [1]
sqr(0) → 0 [1]
add(0, X) → X [1]
terms(N) → cons(recip(sqr(N))) [1]

The TRS has the following type information:

add :: s:0 → s:0 → s:0 s :: s:0 → s:0 half :: s:0 → s:0 0 :: s:0 sqr :: s:0 → s:0 dbl :: s:0 → s:0 first :: s:0 → nil:cons → nil:cons nil :: nil:cons cons :: recip → nil:cons terms :: s:0 → nil:cons recip :: s:0 → recip

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

half
first
terms

(c) The following functions are completely defined:

sqr
dbl
add

Due to the following rules being added:
none

And the following fresh constants:

const

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: add(s(X), Y) → s(add(X, Y)) [1] half(s(0)) → 0 [1] sqr(s(X)) → s(add(sqr(X), dbl(X))) [1] dbl(0) → 0 [1] half(s(s(X))) → s(half(X)) [1] half(0) → 0 [1] first(0, X) → nil [1] dbl(s(X)) → s(s(dbl(X))) [1] first(s(X), cons(Y)) → cons(Y) [1] sqr(0) → 0 [1] add(0, X) → X [1] terms(N) → cons(recip(sqr(N))) [1] The TRS has the following type information: add :: s:0 → s:0 → s:0 s :: s:0 → s:0 half :: s:0 → s:0 0 :: s:0 sqr :: s:0 → s:0 dbl :: s:0 → s:0 first :: s:0 → nil:cons → nil:cons nil :: nil:cons cons :: recip → nil:cons terms :: s:0 → nil:cons recip :: s:0 → recip const :: recip Rewrite Strategy: INNERMOST

(9) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(10) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: add(s(X), Y) → s(add(X, Y)) [1] half(s(0)) → 0 [1] sqr(s(s(X'))) → s(add(s(add(sqr(X'), dbl(X'))), s(s(dbl(X'))))) [3] sqr(s(0)) → s(add(0, 0)) [3] dbl(0) → 0 [1] half(s(s(X))) → s(half(X)) [1] half(0) → 0 [1] first(0, X) → nil [1] dbl(s(X)) → s(s(dbl(X))) [1] first(s(X), cons(Y)) → cons(Y) [1] sqr(0) → 0 [1] add(0, X) → X [1] terms(N) → cons(recip(sqr(N))) [1] The TRS has the following type information: add :: s:0 → s:0 → s:0 s :: s:0 → s:0 half :: s:0 → s:0 0 :: s:0 sqr :: s:0 → s:0 dbl :: s:0 → s:0 first :: s:0 → nil:cons → nil:cons nil :: nil:cons cons :: recip → nil:cons terms :: s:0 → nil:cons recip :: s:0 → recip const :: recip Rewrite Strategy: INNERMOST

(11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
nil => 0
const => 0

(12) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(X)) :|: z = 1 + X, X >= 0
first(z, z') -{ 1 }→ 0 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(X) :|: z = 1 + (1 + X), X >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(X'), dbl(X')), 1 + (1 + dbl(X'))) :|: X' >= 0, z = 1 + (1 + X')
terms(z) -{ 1 }→ 1 + (1 + sqr(N)) :|: z = N, N >= 0

(13) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(14) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

(15) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ first } { dbl } { add } { half } { sqr } { terms }

(16) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {first}, {dbl}, {add}, {half}, {sqr}, {terms}

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z'

(18) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {first}, {dbl}, {add}, {half}, {sqr}, {terms}
Previous analysis results are:

first: runtime: ?, size: O(n1) [z']

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(20) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {half}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z']

(21) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(22) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {half}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z']

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2·z

(24) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {half}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: ?, size: O(n1) [2·z]

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(26) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {add}, {half}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z]

(27) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(28) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {add}, {half}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z]

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(30) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {add}, {half}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: ?, size: O(n1) [z + z']

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(32) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {half}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(33) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(34) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {half}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: half
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(36) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {half}, {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: ?, size: O(n1) [z]

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: half
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(38) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 1 + half(z - 2) :|: z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z]

(39) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(40) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z]

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 1 + 4·z + 4·z²

(42) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: ?, size: O(n2) [1 + 4·z + 4·z2]

(43) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 5 + 22·z + 8·z³

(44) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) :|: z >= 0

Function symbols to be analyzed: {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2]

(45) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(46) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s7) :|: s7 >= 0, s7 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2]

(47) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 3 + 4·z + 4·z²

(48) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s7) :|: s7 >= 0, s7 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {terms}
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: ?, size: O(n2) [3 + 4·z + 4·z2]

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 6 + 22·z + 8·z³

(50) Obligation:

Complexity RNTS consisting of the following rules:

add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + (z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ z }→ 1 + s3 :|: s3 >= 0, s3 <= 1 * (z - 2), z - 2 >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s7) :|: s7 >= 0, s7 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed:
Previous analysis results are:

first: runtime: O(1) [1], size: O(n1) [z'] dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] half: runtime: O(n1) [1 + z], size: O(n1) [z] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: O(n3) [6 + 22·z + 8·z3], size: O(n2) [3 + 4·z + 4·z2]

(51) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(52) BOUNDS(1, n^3)